\begin{tabbing}
$\forall$$k$:Knd, $T$,$B$:Type, $l$:IdLnk, ${\it ds}$:fpf(Id; $x$.Type), ${\it tg}$:Id, $f$:(decl{-}state(${\it ds}$)$\rightarrow$$T$$\rightarrow$$B$).
\\[0ex](($\uparrow$isrcv($k$))
\\[0ex]$\Rightarrow$ ((destination(lnk($k$)) = source($l$) $\in$ Id) $\wedge$ ((lnk($k$) = $l$) $\Rightarrow$ (($T$ = $B$) $\wedge$ (tag($k$) = ${\it tg}$)))))
\\[0ex]$\Rightarrow$ normal{-}ds\=\{i:l\}\+
\\[0ex](${\it ds}$)
\-\\[0ex]$\Rightarrow$ normal{-}type\=\{i:l\}\+
\\[0ex]($T$)
\-\\[0ex]$\Rightarrow$ normal{-}type\=\{i:l\}\+
\\[0ex]($B$)
\-\\[0ex]$\Rightarrow$ es{-}real\=\{i:l\}\+
\\[0ex](${\it es}$.usends1{-}p(${\it es}$;${\it ds}$;$k$;$T$;$l$;${\it tg}$;$B$;$f$))
\-
\end{tabbing}